Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:	qsort(nil)	→ nil
2:	qsort(x . y)	→ qsort(lowers(x,y)) ++ (x . qsort(greaters(x,y)))
3:	lowers(x,nil)	→ nil
4:	lowers(x,y . z)	→ if(y ≤ x,y . lowers(x,z),lowers(x,z))
5:	greaters(x,nil)	→ nil
6:	greaters(x,y . z)	→ if(y ≤ x,greaters(x,z),y . greaters(x,z))

There are 6 dependency pairs:

The approximated dependency graph contains 2 SCCs: {12} and {11}.

Consider the SCC {12}. There are no usable rules. By taking the AF π with π(GREATERS) = 2 and π(.) = [2] together with the lexicographic path order with empty precedence, rule 12 is strictly decreasing.

Consider the SCC {11}. There are no usable rules. By taking the AF π with π(LOWERS) = 2 and π(.) = [2] together with the lexicographic path order with empty precedence, rule 11 is strictly decreasing.

Hence the TRS is terminating.

Tyrolean Termination Tool (0.02 seconds) --- May 4, 2006